#include "ltlf2dfa/syft_ext.h"
#include <cudd/cuddObj.hh>
#include <unordered_map>

bool syft_check_synthesis(SynType which_first, std::string dfa_filename, std::string &partfile)
{
    Cudd mgr;
    bool res = false;
    std::unordered_map<unsigned, BDD> strategy;
    Syft::syn test(&mgr, dfa_filename, partfile);
    bool syn_res = (which_first == SynType::SYS_FIRST) ? test.realizablity_sys(strategy) : test.realizablity_env(strategy);
    return syn_res;
}

bool syft_check_synthesis(SynType which_first, DFA *a, std::string &partfile, int var_num, std::vector<std::string> &var_names,
                          std::vector<char> &var_orders)
{
    char *temp_filename = tmpnam(nullptr);
    printDfaFile(a, string(temp_filename), var_num, var_names, var_orders);
    bool syn_res = syft_check_synthesis(SynType::SYS_FIRST, string(temp_filename), partfile);
    return syn_res;
}
